val(e)  val(e') == valtype(e')  valtype(e) & val(e) = val(e') 

latex

---

clarification:

es-same-val(es;e;e')
== es-valtype(es; e')  es-valtype(es; e) & es-val(es; e) = es-val(es; e')  es-valtype(es; e) 

latex

Definitions	P & Q, A  B, s = t, valtype(e), val(e)
FDL editor aliases	es-same-val